🤖 Gemini PR Summary

This diff represents a major step towards formalizing the security of the FRI protocol, underpinned by a significant refactoring of the algebraic and field theory libraries.

Here is a summary of the key changes:

• Refactoring of Algebra Towers:

  • The custom AlgebraTower class has been renamed and refactored into TowerOfAlgebra and AssocTowerOfAlgebra. This change is propagated throughout the codebase, particularly in the binary field tower implementation.

• Binary Field Tower Implementation:

  • The definitions for both the abstract (BTField) and concrete (ConcreteBTField using BitVec) binary field towers have been heavily reworked for greater clarity and correctness.
  • A formal equivalence between the abstract and concrete tower constructions (AssocTowerOfAlgebraEquiv) has been introduced, though the proofs are still in progress.

• FRI Security Proof Framework:

  • A new file, ArkLib/ProofSystem/BatchedFri/Security.lean, has been added to lay the groundwork for FRI's soundness proof, referencing the "Proximity Gaps for Reed-Solomon Codes" paper.
  • ArkLib/Data/CodingTheory/ProximityGap.lean is significantly expanded with new sections defining concepts like "correlated agreement on a curve" and "weighted agreement," which are crucial for the security analysis.

• Protocol Specification and Cleanup:

  • The FRI protocol's verifier logic and domain definitions have been cleaned up. For instance, the method for generating query points was simplified.
  • The implementation of the Additive NTT (AdditiveNTT/Impl.lean) was removed, likely to streamline focus on the FRI security proof.
  • Several proofs across the coding theory library have been temporarily replaced with sorry, indicating a work-in-progress refactoring.

In essence, this diff strengthens the algebraic foundations and introduces the core theoretical components required to formally prove the security of the FRI protocol.

Analysis of Changes

sorry Tracking

• ❌ Added: 22 sorry(s)
  • theorem weighted_correlated_agreement_for_parameterized_curves' in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma fri_query_soundness in ArkLib/ProofSystem/BatchedFri/Security.lean
  • lemma split_join_via_add_smul_eq_iff_split {k : ℕ} (h_pos : k > 0) in ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean
  • instance {t l : ℕ} : in ArkLib/ProofSystem/BatchedFri/Security.lean
  • theorem weighted_correlated_agreement_for_parameterized_curves in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma isInterleaved_codeOfLinearCode : (codeOfLinearCode κ LC).isInterleaved in ArkLib/Data/CodingTheory/InterleavedCode.lean
  • lemma algebraMap_eq_zero_x {i j : ℕ} (h_le : i < j) (x : BTField i) : in ArkLib/Data/FieldTheory/BinaryField/Tower/Basic.lean
  • lemma fri_round_consistency_completeness in ArkLib/ProofSystem/BatchedFri/Security.lean
  • theorem large_agreement_set_on_curve_implies_correlated_agreement {l : ℕ} in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma list_agreement_on_curve_implies_correlated_agreement_bound in ArkLib/Data/CodingTheory/ProximityGap.lean
  • def hli_level_diff_0 (l : ℕ) : in ArkLib/Data/FieldTheory/BinaryField/Tower/Basic.lean
  • theorem generator_is_not_lifted_to_succ (k : ℕ) : in ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean
  • theorem weighted_correlated_agreement_over_affine_spaces' in ArkLib/Data/CodingTheory/ProximityGap.lean
  • theorem large_agreement_set_on_curve_implies_correlated_agreement' {l : ℕ} in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma sqrt_le_J {q x : ℚ} : in ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
  • theorem unique_linear_decomposition_succ (k : ℕ) : in ArkLib/Data/FieldTheory/BinaryField/Tower/Basic.lean
  • theorem minPoly_of_powerBasisSucc_generator (k : ℕ) : in ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean
  • theorem average_proximity_implies_proximity_of_linear_subspace [DecidableEq ι] [DecidableEq F] in ArkLib/Data/CodingTheory/ProximityGap.lean
  • lemma fri_soundness in ArkLib/ProofSystem/BatchedFri/Security.lean
  • lemma sufficiently_large_list_agreement_on_curve_implies_correlated_agreement in ArkLib/Data/CodingTheory/ProximityGap.lean
  • theorem towerEquiv_commutes_left (i j : ℕ) (h : i ≤ j) : ∀ r : ConcreteBTField i, in ArkLib/Data/FieldTheory/BinaryField/Tower/Impl.lean
  • theorem weighted_correlated_agreement_over_affine_spaces in ArkLib/Data/CodingTheory/ProximityGap.lean

Last updated: 2025-12-09 13:35 UTC. See the main CI run for build status.